perm filename UNIQUE.LSP[W84,JMC] blob
sn#747340 filedate 1984-03-18 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 unique.lsp[w84,jmc] Try at circumscribing unique names in ekl
C00003 ENDMK
C⊗;
unique.lsp[w84,jmc] Try at circumscribing unique names in ekl
(axiom |∀x.equal(x,x)|)
(axiom |∀x y.equal(x,y) ⊃ equal(y,x)|)
(axiom |∀x y z.equal(x,y) ∧ equal(y,z) ⊃ equal(x,z)|)
(axiom |∀P x y.denotational P ∧ P(x) ∧ equal(x,y) ⊃ P(y)|)
(axiom |∀x y. x ≠ y ∧ ¬ab aspect1(x,y) ⊃ ¬equal(x,y)|)
;;; We don't really need this if we circumscribe equal directly.